ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), es:ES, i:Id.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  Valtype(da;kind(e)))
 ecl-es-halt(es;x)  {e:E| loc(e) = i }{e2:E| loc(e2) = i }Prop 

latex

Definitions

x:A. B(x), P  Q, t  T, , Prop, ecl-es-halt(es;x), if b t else f fi, A & B, False, P  Q, P & Q, A, State(ds), x,y. t(x;y), true, x. t(x), state@i, SQType(T), {T}, false, AB, x,y,z,w. t(x;y;z;w), S  T, x,y,z. t(x;y;z), , x(s1,s2), x(s1,s2,s3,s4), x(s1,s2,s3), Unit, P  Q, x(s),

Lemmas

ecl ind wf, nat wf, es-loc wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, es-first-since wf, es-state-when wf, subtype rel dep function, es-vartype wf, fpf-cap wf, Id wf, id-deq wf, top wf, subtype rel self, es-val wf, Knd sq, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, false wf, le wf, decl-state wf, ma-valtype wf, existse-between3 wf, es-first wf, es-pred wf, es-loc-pred, ecl-ex wf, nat plus inc, nat plus wf, ifthenelse wf, eq int wf, existse-between2 wf, l-all wf, le int wf, alle-between1 wf, alle-between2 wf, l member wf, es-pstar-q wf, l exists wf, es-E wf, es-valtype wf, es-kind wf, event system wf, ecl wf, fpf wf, Knd wf